Termination w.r.t. Q proof of TRS/currying/AG01#3.10.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

Q is empty.

↳ QTRS

  ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

Q is empty.

The TRS is overlay and locally confluent. By [15] we can switch to innermost.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(rm, n)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(filter2, app'(f, x)), f), x)
APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(app'(eq, x), y)
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(add, app'(f, x)), app'(app'(map, f), xs))
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(app, app'(app'(rm, n), x)), y)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(app'(add, n), y)
APP'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, m), x))
APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(add, n), x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(if_rm, app'(app'(eq, n), m)), n)
APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(rm, n)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(rm, n), x)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(min, app'(app'(add, n), x))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(filter2, app'(f, x)), f)
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(le, n)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(eq, n)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(filter, f)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(minsort, app'(app'(app, app'(app'(rm, n), x)), y))
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(add, m), app'(app'(rm, n), x))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(filter2, app'(f, x))
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(add, n), app'(app'(app, x), y))
APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x))))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(add, app'(f, x))
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app, app'(app'(rm, n), x))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(map, f), xs)
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(filter, f)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(add, x)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(minsort, x)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(app, x), y)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(app'(minsort, x), app'(app'(add, n), y))
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(if_rm, app'(app'(eq, n), m))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(eq, x)
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app, x)
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(rm, n)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(if_min, app'(app'(le, n), m))
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(add, x), app'(app'(filter, f), xs))
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(eq, n)
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(eq, n), app'(min, app'(app'(add, n), x)))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(le, n), m)
APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(app'(le, x), y)
APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, n), x))
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(le, x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(eq, n), m)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(rm, n)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(filter2, app'(f, x)), f), x)
APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(app'(eq, x), y)
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(add, app'(f, x)), app'(app'(map, f), xs))
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(app, app'(app'(rm, n), x)), y)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(app'(add, n), y)
APP'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, m), x))
APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(add, n), x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(if_rm, app'(app'(eq, n), m)), n)
APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(rm, n)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(rm, n), x)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(min, app'(app'(add, n), x))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(filter2, app'(f, x)), f)
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(le, n)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(eq, n)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(filter, f)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(minsort, app'(app'(app, app'(app'(rm, n), x)), y))
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(add, m), app'(app'(rm, n), x))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(filter2, app'(f, x))
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(add, n), app'(app'(app, x), y))
APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x))))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(add, app'(f, x))
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app, app'(app'(rm, n), x))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(map, f), xs)
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(filter, f)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(add, x)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(minsort, x)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(app, x), y)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(app'(minsort, x), app'(app'(add, n), y))
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(if_rm, app'(app'(eq, n), m))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(eq, x)
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app, x)
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(rm, n)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(if_min, app'(app'(le, n), m))
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(add, x), app'(app'(filter, f), xs))
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(eq, n)
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(eq, n), app'(min, app'(app'(add, n), x)))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(le, n), m)
APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(app'(le, x), y)
APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, n), x))
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(le, x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(eq, n), m)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We deleted some edges using various graph approximations

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(rm, n)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(filter2, app'(f, x)), f), x)
APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(app'(eq, x), y)
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(add, app'(f, x)), app'(app'(map, f), xs))
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(app, app'(app'(rm, n), x)), y)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(app'(add, n), y)
APP'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, m), x))
APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(add, n), x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(if_rm, app'(app'(eq, n), m)), n)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(rm, n), x)
APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(rm, n)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(min, app'(app'(add, n), x))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(filter2, app'(f, x)), f)
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(le, n)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(eq, n)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(filter, f)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(minsort, app'(app'(app, app'(app'(rm, n), x)), y))
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(add, m), app'(app'(rm, n), x))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(filter2, app'(f, x))
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(add, n), app'(app'(app, x), y))
APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x))))
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(add, app'(f, x))
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app, app'(app'(rm, n), x))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(map, f), xs)
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(filter, f)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(add, x)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(minsort, x)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(app'(minsort, x), app'(app'(add, n), y))
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(app, x), y)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(if_rm, app'(app'(eq, n), m))
APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(eq, x)
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app, x)
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(rm, n)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(if_min, app'(app'(le, n), m))
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(eq, n)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(add, x), app'(app'(filter, f), xs))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(eq, n), app'(min, app'(app'(add, n), x)))
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(app'(filter, f), xs)
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(le, n), m)
APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(app'(le, x), y)
APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, n), x))
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil)
APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(le, x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(eq, n), m)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 7 SCCs with 37 less nodes.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(app, x), y)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13]. Here, we combined the reduction pair processor with the A-transformation [14] which results in the following intermediate Q-DP Problem.
Q DP problem:
The TRS P consists of the following rules:

APP(add(n, x), y) → APP(x, y)

R is empty.
The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.

The following pairs can be oriented strictly and are deleted.

APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(app, x), y)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
APP(x1, x2) = APP(x1)
add(x1, x2) = add(x1, x2)

Lexicographic path order with status [19].
Quasi-Precedence:

add₂ > APP₁

Status:

APP₁: [1]
add₂: [1,2]

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(app'(le, x), y)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

LE(s(x), s(y)) → LE(x, y)

R is empty.
The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.

The following pairs can be oriented strictly and are deleted.

APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(app'(le, x), y)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
LE(x1, x2) = LE(x2)
s(x1) = s(x1)

Lexicographic path order with status [19].
Quasi-Precedence:

s₁ > LE₁

Status:

LE₁: [1]
s₁: [1]

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, n), x))
APP'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, m), x))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

MIN(add(n, add(m, x))) → IF_MIN(le(n, m), add(n, add(m, x)))
IF_MIN(false, add(n, add(m, x))) → MIN(add(m, x))
IF_MIN(true, add(n, add(m, x))) → MIN(add(n, x))

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.

The following pairs can be oriented strictly and are deleted.

APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))

The remaining pairs can at least be oriented weakly.

APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, n), x))
APP'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, m), x))

Used ordering: Combined order from the following AFS and order.
MIN(x1) = MIN(x1)
add(x1, x2) = add(x2)
IF_MIN(x1, x2) = x2
le(x1, x2) = le(x1, x2)
false = false
true = true
s(x1) = x1
0 = 0

Lexicographic path order with status [19].
Quasi-Precedence:

le₂ > [MIN₁, add_1]
false > [MIN₁, add_1]
true > [MIN₁, add_1]
0 > [MIN₁, add_1]

Status:

MIN₁: [1]
true: multiset
false: multiset
0: multiset
le₂: [2,1]
add₁: [1]

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, n), x))
APP'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, m), x))

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 0 SCCs with 2 less nodes.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(app'(eq, x), y)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

EQ(s(x), s(y)) → EQ(x, y)

R is empty.
The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.

The following pairs can be oriented strictly and are deleted.

APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(app'(eq, x), y)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
EQ(x1, x2) = EQ(x2)
s(x1) = s(x1)

Lexicographic path order with status [19].
Quasi-Precedence:

s₁ > EQ₁

Status:

EQ₁: [1]
s₁: [1]

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

RM(n, add(m, x)) → IF_RM(eq(n, m), n, add(m, x))
IF_RM(true, n, add(m, x)) → RM(n, x)
IF_RM(false, n, add(m, x)) → RM(n, x)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.

The following pairs can be oriented strictly and are deleted.

APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)

The remaining pairs can at least be oriented weakly.

APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))

Used ordering: Combined order from the following AFS and order.
RM(x1, x2) = RM(x1, x2)
add(x1, x2) = add(x1, x2)
IF_RM(x1, x2, x3) = IF_RM(x2, x3)
eq(x1, x2) = x1
true = true
false = false
0 = 0
s(x1) = s

Lexicographic path order with status [19].
Quasi-Precedence:

0 > true
s > false > [RM₂, IF_{RM_2]} > add₂

Status:

true: multiset
false: multiset
add₂: [1,2]
0: multiset
s: []
RM₂: [1,2]
IF_RM₂: [1,2]

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 0 SCCs with 1 less node.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(app'(minsort, x), app'(app'(add, n), y))
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(map, f), xs)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(app'(filter, f), xs)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(map, f), xs)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)

The remaining pairs can at least be oriented weakly.

APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(app'(filter, f), xs)

Used ordering: Combined order from the following AFS and order.
APP'(x1, x2) = APP'(x2)
app'(x1, x2) = app'(x1, x2)
map = map
add = add
filter2 = filter2
true = true
filter = filter
false = false
if_minsort = if_minsort
minsort = minsort
eq = eq
min = min
if_rm = if_rm
rm = rm
app = app
s = s
nil = nil
0 = 0
le = le
if_min = if_min

Lexicographic path order with status [19].
Quasi-Precedence:

[APP'₁, filter2] > [map, add, true, nil, le] > filter > [app'₂, app] > [eq, rm, s]
[APP'₁, filter2] > [map, add, true, nil, le] > false > [app'₂, app] > [eq, rm, s]
[APP'₁, filter2] > [map, add, true, nil, le] > if_minsort > minsort > min > [app'₂, app] > [eq, rm, s]
[APP'₁, filter2] > [map, add, true, nil, le] > if_rm > [app'₂, app] > [eq, rm, s]
[APP'₁, filter2] > [map, add, true, nil, le] > if_min > min > [app'₂, app] > [eq, rm, s]
0 > [eq, rm, s]

Status:

app'₂: [2,1]
map: multiset
eq: multiset
APP'₁: [1]
min: multiset
app: multiset
0: multiset
rm: multiset
s: multiset
nil: multiset
add: multiset
if_min: multiset
true: multiset
filter: multiset
if_rm: multiset
if_minsort: multiset
false: multiset
le: multiset
filter2: multiset
minsort: multiset

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(app'(filter, f), xs)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 0 SCCs with 2 less nodes.